rcv($l$,${\it tg}$) declared in $M$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\uparrow$fpf{-}dom(KindDeq; rcv($l$,${\it tg}$); (($M$.2).1))